$\forall$${\it es}$:ES, $i$, $x$:Id, $T$:Type, $v$:$T$.
\\[0ex]@$i$ $x$ initially $v$:$T$ $\Rightarrow$ @$i$ only [] affect $x$:$T$ $\Rightarrow$ $\forall$$e$@$i$. ($x$ when $e$) = $v$